Search for: All records

Safety-critical real-time systems require correctness to be validated beyond the design phase. In these systems, response time is as critical as correct functionality. Runtime verification is a promising approach for validating the correctness of system behaviors during runtime using monitors derived from formal system specifications. However, practitioners often lack formal method backgrounds, and no standard notation exists to capture system properties that serve their needs. To encourage the adoption of formal methods in industry, we present GROOT, a runtime monitoring tool for real-time systems that automatically generates efficient monitors from structured English statements. GROOT is designed with two branches, one for functional requirements and one for specifications with metric time constraints, which use appropriate formalisms to synthesize monitors. This paper introduces TIMESPEC, a structured English dialect for specifying timing requirements. Our tool also automates formal analysis to certify the C monitors’ construction. We apply GROOT to timing specifications from an industrial component and a simulated autonomous system in Simulink. 

Record linkage, often called entity resolution or de-duplication, refers to identifying the same entities across one or more databases. As the amount of data that is generated grows at an exponential rate, it becomes increasingly important to be able to integrate data from several sources to perform richer analysis. In this paper, we present an open source comprehensive end to end hybrid record linkage framework that combines the automatic and manual review process. Using this framework, we train several models based on different machine learning algorithms such as random forests, linear SVM, Radial SVM, and Dense Neural Networks and compare the effectiveness and efficiency of these models for record linkage in different settings. We evaluate model performance based on Recall, F1-score (quality of linkages) and number of uncertain pairs which is the number of pairs that need manual review. We also test our trained models in a new dataset to test how different trained models transfer to a new setting. The RF, linear SVM and radial SVM models transfer much better compared to the DNN. Finally, we study the effect of name2vec (n2v) feature, a letter embedding in names, on model performance. Using n2v results in smaller manual review set with slightly less F1-score. Overall the SVM models performed best in all experiments.